package nl.cwi.arne.generator;

import java.io.File;
import java.io.IOException;
import java.io.PrintStream;
import java.util.List;
import java.util.Set;

import nl.cwi.arne.Network;
import nl.cwi.arne.NetworkActivation;
import nl.cwi.arne.generator.mcrl2.ArneMCRL2Translator;
import nl.cwi.arne.generator.util.ActivationEquivalenceClasses;
import nl.cwi.arne.lts.State;
import nl.cwi.arne.lts.resource.LTSResource;
import nl.cwi.arne.lts.util.StableRegionsUtil;
import nl.cwi.arne.mcrl2.Specification;
import nl.cwi.arne.mcrl2.toolchains.GenerateLPSToolChain;
import nl.cwi.arne.mcrl2.toolchains.GenerateLTSToolChain;
import nl.cwi.arne.mcrl2.toolchains.VerifyFormulaToolChain;
import nl.cwi.arne.mcrl2.util.MCRL2FileUtil;
import nl.cwi.arne.mcrl2.util.MCRL2Options;
import nl.cwi.arne.util.NetworkActivationBuffer;
import nl.cwi.arne.util.NetworkActivationComparator;
import nl.cwi.arne.util.NetworkActivationIterator;

import org.eclipse.core.runtime.IProgressMonitor;
import org.eclipse.core.runtime.IStatus;
import org.eclipse.core.runtime.NullProgressMonitor;
import org.eclipse.core.runtime.Status;
import org.eclipse.core.runtime.SubProgressMonitor;
import org.eclipse.emf.common.util.URI;

/**
 * @author Christian Krause
 */
public class NetworkActivationGenerator {

	// Output stream:
	private PrintStream out;

	// Debug flag:
	private boolean debug = false;
	
	// Temporary MCF file:
	private File mcfFile;
	
	// MCRL2 options:
	private MCRL2Options mcrl2Options = new MCRL2Options();
	
	// MCRL2 translator:
	private ArneMCRL2Translator translator = new ArneMCRL2Translator();
	
	// Equivalence classes:
	private ActivationEquivalenceClasses classes;
	
	/**
	 * Generate network activations.
	 * @param network Network.
	 * @param buffer Buffer.
	 * @param monitor Monitor.
	 * @return Status.
	 */
	public IStatus generate(Network network, NetworkActivationBuffer buffer, IProgressMonitor monitor) {
		
		// We need an iterator and a comparator:
		NetworkActivationIterator iterator = new NetworkActivationIterator(network);
		NetworkActivationComparator comparator = new NetworkActivationComparator();
		monitor.beginTask("Generating activations...", ((int) iterator.getMaxCount()) * 2);
		
		// Tidy up first:
		clearTempFiles();
		
		// Get the last network activation, if existing:
		NetworkActivation last = null;
		if (!network.getActivations().isEmpty()) {
			last = network.getActivations().get(network.getActivations().size()-1);
		}
		
		// Some flags, modal formula and mcf-file:
		boolean checkEquivalence = network.isCheckEquivalence();
		boolean checkIslands = network.isCheckStableRegions();
		String formula = network.getModalFormula();
		if (formula!=null && formula.trim().length()==0) {
			formula = null;
		}
		mcfFile = network.isCheckModalFormula() ? MCRL2FileUtil.saveFormula(formula) : null;
		
		// Update the MCRL2 options:
		mcrl2Options.setLpssumelm(true);
		mcrl2Options.setLtsinfo(true);
		
		// Equivalence classes:
		classes = new ActivationEquivalenceClasses(mcrl2Options.getEquivalence());
		
		// Generate the activations:
		int filteredOut = 0;
		int generated = 0;
		while (iterator.hasNext()) {
						
			// Generate the next activation:
			NetworkActivation activation = iterator.next();
			
			// Notify the monitor about the skipped entries:
			monitor.worked(2 * (int) iterator.getSkipped());
			
			// Check if we should skip this one as well:
			if (last!=null) {
				if (comparator.compare(activation, last)<=0) {
					monitor.worked(2); // Current is still smaller or equal than the last in the list.
					continue;
				} else {
					last = null; // Current is bigger.
				}
			}
			
			try {

				// Generate LPS if required:
				File lpsFile = null;
				if (checkEquivalence || checkIslands || mcfFile!=null) {
					lpsFile = generateLPS(activation).getLPSFile();
				}

				// Check the modal formula:
				if (mcfFile!=null) {
					VerifyFormulaToolChain verifyToolchain = verifyFormula(lpsFile, new SubProgressMonitor(monitor,1));
					if (verifyToolchain.getResult()==false) {
						activation = null;
					}
				} else {
					monitor.worked(1);
				}

				// Generate the LTS:
				GenerateLTSToolChain ltsToolchain = null;
				if (activation!=null && (checkEquivalence || checkIslands)) {
					ltsToolchain = generateLTS(lpsFile, new SubProgressMonitor(monitor,1));
				} else {
					monitor.worked(1);
				}

				// LPS file not needed anymore:
				if (lpsFile!=null) {
					lpsFile.delete();
				}

				// Check stable regions?
				if (activation!=null && checkIslands) {
					LTSResource resource = new LTSResource(URI.createFileURI(ltsToolchain.getLTSFile().getAbsolutePath()));
					try {
						resource.load(null);
						int required = network.getStableRegions();
						List<Set<State>> regions = StableRegionsUtil.getStableRegions(resource.getLTS());
						if (required>=0 && regions.size()<required) activation = null;
					} catch (IOException e) {
						ArneGeneratorPlugin.getInstance().logError("Error loading LTS", e);
					}
				}

				// Compare it with the other LTSs:
				if (activation!=null && checkEquivalence) {

					// Get the equivalence class:
					List<NetworkActivation> clazz = classes.add(activation, ltsToolchain.getLTSFile(), 
							ltsToolchain.getNumberOfStates(), ltsToolchain.getNumberOfTransitions());

					// Filter out if there are already equivalent ones:
					if (clazz.size()>1) {
						activation = null;
					}
				}

				// Add it to the buffer it is still there:
				if (activation!=null) {
					buffer.add(activation);
					generated++;
					if (out!=null) {
						out.println(activation);
					}
				} else {
					filteredOut++;
				}

			} catch (Throwable t) {
				buffer.commit();
				clearTempFiles();
				return new Status(IStatus.ERROR, ArneGeneratorPlugin.PLUGIN_ID, "Error generating activations", t);
			}

			// Update the monitor:
			String msg = "Generated " + generated + " activations";
			if (checkEquivalence || checkIslands || mcfFile!=null) msg = msg + " (" + filteredOut + " filtered out)";
			monitor.subTask(msg + "...");
			if (monitor.isCanceled()) {
				buffer.commit();
				clearTempFiles();
				return Status.CANCEL_STATUS;
			}
						
		}
		
		// Flush the buffer a last time.
		buffer.commit();		
		monitor.done();
		return Status.OK_STATUS;
		
	}

	/*
	 * Generate a LPS from a network activation.
	 */
	private GenerateLPSToolChain generateLPS(NetworkActivation activation) {
		Specification spec = translator.generateSpecification(activation);
		GenerateLPSToolChain toolchain = new GenerateLPSToolChain(spec, mcrl2Options);
		toolchain.setProduceSubTasks(false);
		if (debug) {
			toolchain.setOutputStream(out);
		}
		IStatus status = toolchain.execute(new NullProgressMonitor());
		if (status.getSeverity()!=IStatus.OK) {
			throw new RuntimeException(status.getMessage());
		}
		return toolchain;
	}
	
	/*
	 * Generate an LTS.
	 */
	private GenerateLTSToolChain generateLTS(File lpsFile, IProgressMonitor monitor) {
		GenerateLTSToolChain toolchain = new GenerateLTSToolChain(lpsFile, mcrl2Options);
		toolchain.setProduceSubTasks(false);
		if (debug) {
			toolchain.setOutputStream(out);
		}
		IStatus status = toolchain.execute(monitor);
		if (status.getSeverity()!=IStatus.OK) {
			throw new RuntimeException(status.getMessage());
		}
		return toolchain;
	}
	
	/*
	 * Verify a formula.
	 */
	private VerifyFormulaToolChain verifyFormula(File lpsFile, IProgressMonitor monitor) {
		VerifyFormulaToolChain toolchain = new VerifyFormulaToolChain(lpsFile, mcfFile, mcrl2Options);
		toolchain.setDeleteMCFFile(false);
		toolchain.setProduceSubTasks(false);
		if (debug) {
			toolchain.setOutputStream(out);
		}
		IStatus	status = toolchain.execute(monitor);
		if (status.getSeverity()!=IStatus.OK) {
			ArneGeneratorPlugin.getInstance().getLog().log(status);
		}
		return toolchain;
	}
	
	/**
	 * Clear all temporary files.
	 */
	public void clearTempFiles() {
		if (classes!=null) {
			for (File ltsFile : classes.getLTSFileIndex().getAll()) {
				ltsFile.delete();
			}
			classes.getLTSFileIndex().clear();
		}
		if (mcfFile!=null) {
			mcfFile.delete();
			mcfFile = null;
		}
	}
	
	public void setOutputStream(PrintStream out) {
		this.out = out;
	}
	
	public void setMCRL2Options(MCRL2Options mcrl2Options) {
		this.mcrl2Options = mcrl2Options;
	}
	
	public void setTranslator(ArneMCRL2Translator translator) {
		this.translator = translator;
	}
	
	public ActivationEquivalenceClasses getEquivalenceClasses() {
		return classes;
	}

	public void setDebug(boolean debug) {
		this.debug = debug;
	}
	
}
